include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/types.ma".
include "basics/deqsets.ma".
include "basics/lists/list.ma".

inductive Atom: Type[0] ≝
   Name  : nat → Atom
 | CoName: nat → Atom .

(* Atom: notation and interpretation *)
interpretation "Name" 'Name n = (Name n).
notation "hvbox(𝔸 \sub n)" with precedence 90 for @{ 'Name $n }.

(* Negative atom: notation and interpretation *)
notation "hvbox(𝔹 \sub n)" with precedence 90 for @{ 'CoName $n }.
interpretation "CoName" 'CoName n = (CoName n).

(* Atom sets *)

definition Atomeqb ≝ λa,b:Atom.
  match a with 
  [ Name   n ⇒ match b with 
               [ Name   m ⇒ (eqb n m)
               | _        ⇒ false]
  | CoName n ⇒ match b with 
               [ CoName m ⇒ (eqb n m)
               | _        ⇒ false]].
               
notation < "a == b" non associative with precedence 45 for @{Atomeqb $a $b }.

definition Atomneg ≝ λa:Atom.
  match a with 
  [ Name   n ⇒ CoName n
  | CoName n ⇒ Name   n  ].

lemma Atomneg_idemp : ∀ a: Atom. Atomneg (Atomneg a) = a.
#a cases a #N normalize @refl qed .

lemma Atomeqb_true: ∀a,b. iff (Atomeqb a b = true) (a = b).
(* Ho guardato la dimostrazione del lemma 
   beqitem_true in chapter7.ma del tutorial. *)
#a elim a -a
#X #b cases b -b
#Y %
[1,3,5,7: #H normalize in H; destruct 
          (* applico theorem eqb_true_to_eq: 
                        ∀n,m:nat. eqb n m = true → n = m.
             in rithmetics/nat.ma *)
          lapply (eqb_true_to_eq X Y H) -H
          #Heq <Heq @refl
|2,4,6,8: #H normalize destruct
         (* applico theorem eqb_n_n: ∀n. eqb n n = true.
            in rithmetics/nat.ma *)
          @(eqb_n_n Y)
] qed .


(* Si dovrebbe arrivare a dimostrare che due atomi o sono uguali,
o sono diversi, mettendo in evidenza la decidibilità della eguaglianza == *)

definition AtomSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.






inductive Structure : Type[0] ≝
|  unit  : Structure
|  par   : AtomSet → Structure
|  seq   : AtomSet → Structure
|  cop   : AtomSet → Structure
|  mpar  : list Structure → Structure
|  mseq  : list Structure → Structure
|  mcop  : list Structure → Structure
.


definition Structureeqb ≝ λa,b:Atom.
notation < "a ≡ b" non associative with precedence 45 for @{Atomeqb $a $b }.


(* Abbozzo di un'altra via per definire le strutture come insiemi
o poco più, ma non ho indagato oltre. In effetti non sono ottimista
rispetto alla possibilità di definire dei costruttori che alla fine
abbiamo un numero arbitrario di argomenti. L'unico modo sembra
proprio il dover passare per le liste.... *)

inductive Unit: Prop ≝  
mkUnit : Unit.
(* Unit: notation and interpretation *)
interpretation "Unit" 'Unit = Unit.
notation "𝟙" with precedence 90 for @{ 'Unit }.

(* Par *)
inductive Par (A,B:Prop) : Prop ≝
    mkPar : A → B → Par A B.

(* Seq *)
inductive Seq (A,B:Prop) : Prop ≝
    mkSeq : A → B → Seq A B.

(* CoP *)
inductive CoP (A,B:Prop) : Prop ≝
    mkCoP : A → B → CoP A B.




inductive Not (A:Prop): Prop ≝
nmk: (A → False) → Not A.

interpretation "logical not" 'not x = (Not x).




definition name   ≝ λA:Type[0].λx,a:A.〈 x=a, true 〉.
interpretation "name" 'name x = (name ? x).
notation "x+" with precedence 100 for @{name $x}.  
definition coname ≝ λA:Type[0].λx,a:A.〈 x=a, false 〉.
interpretation "singleton" 'coname x = (coname ? x).
notation "x-" with precedence 100 for @{coname $x}.

(* check name.   *)

definition a_a ≝ name nat 1. definition a_b ≝ name nat 2.
definition a_c ≝ name nat 3. definition a_d ≝ name nat 4.
definition ca_a ≝ coname nat 1. definition ca_b ≝ coname nat 2.
definition ca_c ≝ coname nat 3. definition ca_d ≝ coname nat 4.



inductive operator : Type[0] ≝
  mkpar : operator
| mkcopar : operator
| mkseq : operator.  

definition par_base (A:Type[0]) (P:A→Prop×bool) (Q:A→Prop×bool) ≝ 
 λ a:A. 
  match \snd (P a)  with
  [ false ⇒ false
  | cons a tl ⇒ (x == a) ∨ memb S x tl
  ].


let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
  match l with
  [ nil ⇒ false
  | cons a tl ⇒ (x == a) ∨ memb S x tl
  ].



λA,P,Q,a.P a ∨ Q a.
interpretation "union" 'union a b = (union ? a b).




